Inference at * 1 1 
Iof proof for Lemma decidable atom equal:



1. a : Atom
2. b : Atom
  if a=b then inl Ax  else (inr (x.x) )  ((a = b)  ((a = b))) 

latex

 by MemberEqCD 

latex

 1: .....subterm..... T:t1:n

 1:   a  Atom
 2: .....subterm..... T:t2:n

 2:   b  Atom
 3: .....subterm..... T:t3:n

 3: 3. a = b
 3:   (inl Ax )  ((a = b)  ((a = b)))
 4: .....subterm..... T:t4:n

 4: 3. (a = b)
 4:   (inr (x.x) )  ((a = b)  ((a = b)))
 .

Definitions

t  T, P  Q, False, A